/*
 * Backtracker.cuh
 *
 *  Created on: Oct 3, 2013
 *      Author: jaime
 */

#ifndef BACKTRACKER_CUH_
#define BACKTRACKER_CUH_

#include "VariablesStateHandler.cuh"
#include "../BCPStrategy/WatchedClausesList.cuh"
#include "../ConflictAnalysis/CUDAListGraph.cuh"
#include "../Statistics/RuntimeStatistics.cuh"

class Backtracker {
private:
	VariablesStateHandler* variables_handler;
	WatchedClausesList * watched_clauses;
	CUDAListGraph * graph;
#ifdef ENABLE_STATISTICS
	RuntimeStatistics * stats;
#endif

	__device__ void backtrack_to(int decision_level);

public:
	__device__ Backtracker(VariablesStateHandler* handler,
			WatchedClausesList * watched_clauses, CUDAListGraph * graph
#ifdef ENABLE_STATISTICS
			,RuntimeStatistics * stats
#endif
	);

	__device__ sat_status handle_backtrack(int decision_level, bool switch_literal);
	__device__ sat_status handle_backtrack(int decision_level);
	__device__ void set_watched_clauses(WatchedClausesList * watched_clause);

	__device__ sat_status handle_chronological_backtrack();


};

#endif /* BACKTRACKER_CUH_ */
